Inference at * 1 1 0 
Iof proof for Lemma assert of le int:



1. x : 
2. y : 
  ((y <z x))  ((y < x)) 

latex

 by PERMUTE{1:n, 2:n, 2:n, 2:n, 3:n, 4:n, 5:n, 6:n, 7:n, 8:n} 

latex

 1: .....wf..... NILNIL

 1:   ((y <z x))  
 2: .....wf..... NILNIL

 2:   ((y < x))  
 3: .....wf..... NILNIL

 3:   (y <z x)  
 4: .....wf..... NILNIL

 4:   (y < x)  
 5: .....wf..... NILNIL

 5:   y  
 6: .....wf..... NILNIL

 6:   x  
 7: .....wf..... NILNIL

 7:   ((y < x)) = ((y < x))
 8: 

 8:   ((y < x))  ((y < x))
 .

Definitions	t  T, x:A  B(x), Type, f(a), s = t, x:AB(x), , a < b, i <z j, b, A, , x:A. B(x), P  Q, P  Q, P  Q, P  Q
Lemmas	assert of lt int, not functionality wrt iff, iff functionality wrt iff